the_es:ES, e, e':E. (e <loc e') & (e1:E. ((e <loc e1) & (e1 <loc e')))  e = pred(e') 

latex

Definitions	A & B, x:A. B(x), E, t  T, (e <loc e'), Prop, A, P  Q, P & Q, ES, first(e), b, False, P  Q, pred(e), P  Q, P  Q, loc(e), Id
Lemmas	es-loc-pred, Id wf, es-loc wf, es-pred wf, assert wf, es-first wf, event system wf, es-axioms, not wf, es-locl wf, es-E wf